<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD><TITLE>Notes</TITLE>

<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.09">
<LINK rel="stylesheet" type="text/css" href="Reference-Manual.css">
</HEAD>
<BODY >
<HR CLASS="footnoterule"><DL CLASS="thefootnotes"><DT CLASS="dt-thefootnotes">
<A NAME="note19" HREF="Reference-Manual013.html#text19">1</A></DT><DD CLASS="dd-thefootnotes">which are the levels effectively chosen in the
current implementation of <SPAN STYLE="font-variant:small-caps">Coq</SPAN>
</DD><DT CLASS="dt-thefootnotes"><A NAME="note20" HREF="Reference-Manual013.html#text20">2</A></DT><DD CLASS="dd-thefootnotes">
<SPAN STYLE="font-variant:small-caps">Coq</SPAN> accepts notations declared as no associative but the parser on
which <SPAN STYLE="font-variant:small-caps">Coq</SPAN> is built, namely <SPAN STYLE="font-variant:small-caps">Camlp4</SPAN>, currently does not implement the
no-associativity and replace it by a left associativity; hence it is
the same for <SPAN STYLE="font-variant:small-caps">Coq</SPAN>: no-associativity is in fact left associativity
</DD><DT CLASS="dt-thefootnotes"><A NAME="note21" HREF="Reference-Manual013.html#text21">3</A></DT><DD CLASS="dd-thefootnotes">Tactic notations are just a simplification of
the <TT>Grammar tactic simple_tactic</TT> command that existed in
versions prior to version 8.0.
</DD></DL>

</BODY></HTML>
